i:Id, A:MsgA, P:(Id), L:({loc:Id| P(loc) }(MsgA List)).
(loc:Id. (A,Bif P(loc) L(loc) else nil fi.A ||+ B))
 P(i)
 (n:||L(i)||. A  L(i)[n]  @i: A  loc.(if P(loc) L(loc) else nil fi)) 

latex

Definitions	Id, MsgA, x(s), if b t else f fi, A ||+ B, (x,yL.P(x;y)), x:A. B(x), P  Q, t  T, b, Prop, x,y. t(x;y), , ||as||, False, A, P & Q, AB, i  j < k, {i..j}, (L), M1  M2, b, P  Q, {T}, SQType(T), P  Q, l[i], Unit, a = b, , M(i), D1  D2, @i: A, (x  l)
Lemmas	length wf2, ma-sub-join-list, select member, ma-sub transitivity, ma-sub wf, select wf, not functionality wrt iff, assert-eq-id, eq id wf, ma-empty-sub, ma-join-list wf, length wf1, int seg wf, Id sq, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, assert wf, Id wf, pairwise wf, ifthenelse wf, ma-compat wf, msga wf